#[thrust_macros::context]
impl<T> VecWrap<T> {
  #[thrust::trusted]
  #[thrust_macros::requires(index < (*self).1)]
  #[thrust_macros::ensures(*result == (*self).0[index])]
  fn get(&self, index: usize) -> &T {
      &self.inner[index]
  }
}

impl<T> VecWrap<T> {
    #[thrust::ignored]
    #[thrust::_impl_context(impl < T > VecWrap < T > {})]
    fn len(&self) -> usize { self.inner.len() }
    #[allow(unused_variables)]
    #[allow(non_snake_case)]
    #[thrust::formula_fn]
    fn _thrust_requires_len(self_: <&Self as thrust_models::Model>::Ty)
        -> bool where T: thrust_models::Model,
        <T as thrust_models::Model>::Ty: PartialEq {
        true
    }
    #[allow(unused_variables)]
    #[allow(non_snake_case)]
    #[thrust::formula_fn]
    fn _thrust_ensures_len(result: <usize as thrust_models::Model>::Ty,
        self_: <&Self as thrust_models::Model>::Ty) -> bool where
        T: thrust_models::Model, <T as thrust_models::Model>::Ty: PartialEq {
        (true) && (result == (*self_).1)
    }
    #[thrust::extern_spec_fn]
    #[allow(path_statements)]
    fn _thrust_extern_spec_len(&self) -> usize where T: thrust_models::Model,
        <T as thrust_models::Model>::Ty: PartialEq {

        #[thrust::requires_path]
        Self::_thrust_requires_len;

        #[thrust::ensures_path]
        Self::_thrust_ensures_len;
        Self::len(self)
    }
}